basic
\\[0ex]Refl($T$;$x$,$y$.$E$($x$;$y$)) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$a$:$T$. $E$($a$;$a$)